﻿Теоремы разложения
admin|2009/01/15 23:56:44
##PAGE##
 Теоремы разложения это утверждения, позволяющие придать
нерекурсивную форму, функциям определенным при помощи рекурсивных
уравнений. Доказательство этих теорем часто заметно сложнее
доказательства законов, описанных выше, так как ведется не на языке
алгебры программ, а на языке минимальных неподвижных точек
непрерывных функционалов. Создавая свою алгебру программ, Бэкус
предполагал, что такого рода законы будут исследоваться
профессиональными математиками, а программисты будут лишь
пользоваться полученными результатами. В соответствии с этим
подходом, мы вводим многие понятия неформально и не приводим здесь
доказательств большинства используемых теорем, интересующийся
читатель всегда сможет найти их в cite{backus77},cite{backus81},cite{Williams80}.
==Формы==
 Для начала неформально введем понятие "формы", которые мы
используем по ходу этого раздела. 

Форма это схема программы,
полученная путем замены функций f, g, h на функциональные символы
<math>f</math>, <math>g</math>, <math>h</math>, то есть по сути абстракцией по этим функциям.
Обозначается как <math>Hfgh</math>. Программа, полученная путем подстановки
конкретных функций f,g, h в форму <math>Hfgh</math> обозначается,
соответственно <math>H</math>fgh.

Если форма зависит только от одной переменной, то вводится понятие
композции форм: если Gf и Hf - формы, то композицией G и H, которая
обозначается через GH называется результат замены переменной <math>f</math> в
форме G на H. Например, если
<math> Gf = f\circ r , Hf = p\rightarrow;f</math>
то <math>GHf = (p\rightarrow q;f)\circ r , Hgf = p\rightarrow g;f \circ r</math>
 Надо быть осторожным и не путать композицию функций и композицию
форм, особенно когда композиция функций используется для построения
форм. Композиция GG может обозначаться <math>G^2</math>, соответственно.
композиция <math>G \ldots G</math> будет обозначаться <math>G^n</math>.

==Общая теорема разложения==
====Понятие разложения====
 Пусть <math>E</math> - форма,


<math>
f_0=\bar{\bot}\\
f_{i+1}=p\rightarrow q_0;\ldots;p_i\rightarrow q_i;\bar{\bot}\\
</math>
при i = 0,1,..,<math> p_i, q_i in F.</math>

Пусть E обладает тем свойством, что
<math> E(f_i)=f_{i+1} </math>при i = 0,1,... .
Тогда форма E называется ''разложимой с аппроксимирующими
функциями ''<math>f_i</math>. 

Мы пишем
<math>f=p_0\rightarrow;\ldots;p_n\rightarrow q_m;ldots.</math>
чтобы указать, что <math>f=lim_{i\to\infty}{f_i}</math>, где <math>f_i</math> имеет
приведенный выше вид. Правую часть мы называем ''бесконечным
разложением'' для <math>f</math>. Будем считать, что <math>f:x</math> определено тогда и
только тогда, когда существует значение <math>n\geq 0</math>, такое, что 
*<math>p_1:x=F</math> для всех <math>i\le n</math> и 
*<math>p_n:x = T</math> и
*<math>q_n:x</math> определено; в таком случае <math>f:x=q_n:x</math>

 В основополагаюшей статье cite{backus77} Бэкус сформулировал общую
теорему разложения. Она не так удобна, как более частные (и более
развитые!) методы, описанные ниже, но иногда также позволяет
получить полезные результаты.

====Теорема о разложении==== 
Пусть форма <math>E</math>, разложимая с указанными
выше аппроксимирующими функциями. Пусть <math>f</math> - наименьшая функция,
удовлетворяющая <math>f=E(f)</math>.

 Тогда
<math>f=p_0\rightarrow;\ldots;p_n\rightarrow q_m;\ldots.</math>

=====Доказательство.===== 
Поскольку <math>E</math> - это композиция непрерывных
функционалов (все комбинирующие формы непрерывны), включающих только
строгие функции в качестве константных членов, то функция E
непрерывна (см \cite{IndMeth} для уточения и строгих доказательств).
Поэтому ее наименьшая фиксированная точка <math>f</math> имеет вид
<math>f=\lim_{i\to\infty}{E^i(\bar{\bot})}=\lim_{i\to\infty}{f_i}</math>, а по
определению это и есть указанное выше бесконечное разложение для
<math>f</math>.

В таком же духе Бэкус формулирует и полезную теорему о линейном
разложении, но мы будем использовать более позднюю и более ясную
версию, сформулированную в следующем разделе.

==Теорема о линейном расширении и ее следствия==
 В этом подразделе описывается важный и наиболее исследованный класс программ
- программы которые которые подходят по определение линейной формы.
Изложение ведется согласно работе \cite{backus81}, где Бэкус обобщил и упростил соответствующие
результаты статьи ~\cite{backus77}.

===Линейные формы и линейное разложение===
'''Определение.'''Форма <math>Hf</math> является линейной по <math>f</math> если
существует такая форма <math>H_1f</math>, такая что для всех функци <math>a</math> ,<math>b</math> и
<math>c</math>, выполняется <math>H(a\rightarrow b;c)=H_1a\rightarrow Hb;Hc</math>. В этом
случае форма <math>H_1f</math> связанная с формой </math>Hf</math> называется предикатным
преобразователем.

 Класс функций, подпадающих под этот определение
оказывается очень обширным. Бэкус\cite{backus81} также сумел
доказать линейность различных комбинаций линейных форм и найти
методы получения предикатного преобразователя таких форм. В силу
этого, весьма полезной оказывается следующая теорема:

===Теорема о линейном расширении===
 Если
<math>f=p\rightarrow q;Hf$</math> и <math>$H$</math> является строгой и линейной формой, то
<math>f = p\rightarrow q\ldots;H^n_1p\rightarrow H^nq;\ldots</math>.

 Для того, чтобы продемонстрировать применение этой теоремы,
приведем пример доказательства свойств программы, при помощи двух ее
частных случаев - теоремы о рекурсии и теоремы об итерации.

====Теорема о рекурсии====
 Теорема о рекурсии была сформулирована первый раз в работе
 \cite{backus77} следующим образом:

 Пусть <math>f</math> является решением для
<math>f=p\rightarrow q; Qf ,Q=h\circ[i,f\circ j] </math>
  
 Тогда <math>f</math> представимо в виде
<math>f=p\rightarrow q;\ldots;p\circ j^n\rightarrow Q^nq</math>

где <math>Q^ng = h\circ[i, Q^{n-1}g\circ j]=/h\circ[i,i\circ
j,\ldots,i\circ j^{n-1},g\circ j ^n]</math>

'''Доказательство'''.

 Согласно результатам работы \cite{backus81}
форма Q линейна, поскольку она является композицией базисных
линейных форм, и предикатный преобразователь <math>Q_t</math> имеет вид <math>Q_tf=
f\circ j</math>. В соответствии с теоремой линейного расширения
<math>f=p\rightarrow q;\ldots;p\circ j^n\rightarrow Q^nq</math>.

'''Пример.''' Используем теорему о рекурсии для доказательства
корректности рекурсивной факториальной функции. 

Пусть <math>f</math>- решение
для 
<math>f=eq0\rightarrow \bar{1};\times\circ[id,f\circ subl]</math>
 
Тогда f удовлетворяет формулировке теоремы о рекурсии для 
<math>p = eq0,g=\bar{1},h=\times,i=id , j=s</math>.

Поэтому<math>f=eq0\rightarrow \bar{1};\ldots;eq0\circ subl^n\rightarrow
Q^n\bar{1}</math>и 

<math>Q^n\bar{1}=/\times[id,id\circ subl,\ldots,id\circ
subl^{n-1},\bar{1}\circ subl^n]</math>

 Теперь <math>id\circ subl^k=subl^k</math> по
[III.2] и <math>eq0\circ subl^n\rightarrow\rightarrow\bar{1}\circ
subl^n=\bar{1}</math> согласно [III.1], поскольку <math>eq0\circ
subl^n:x=eq0(x-n)\equiv x=n</math>, то если <math>eq0\circ subl^n:x=T</math>, то
<math>x=n</math> и

<math>Q^n\bar1:n=n\times(n-1)\times\ldots\times(n-(n-1))\times(\bar{1}:(n-n))=n!</math>

====Теорема об итерации====
 Теперь сформулируем теорему об итерации и с ее помощью докажем
корректность итеративной версии программы вычисления факториала.

'''Теорема об итерации.''' Пусть <math>f</math>-это решение (т.е. наименьшее
решение) для

 <math>f=p\rightarrow g; h\circ f\circ k </math>

 Тогда
<math>f=p\rightarrow g; p\circ k\rightarrow h\circ g\circ k;\ldots;p\circ k^n\rightarrow h^n\circ g\circ k^n;\ldots</math>

'''Доказательство'''. Пусть <math>h'=h\circ2</math>, <math>i'=id</math>, <math>j'=k</math>. Тогда

<math>f=p\rightarrow g;h'\circ[i',f\circ j']</math>

поскольку <math>h\circ2\circ[id,f\circ k]=h\circ f\circ k</math> по [I.5].
Итак, теорема о рекурсии дает <math>f=p\rightarrow g;\ldots;p\circ
k^n\rightarrow Q^ng</math> где

<math>
Q^ng=h\circ2\circ[id, Q^{n-1}g\circ k]\\
    =h\circ Q^{n-1}\circ k=h^n\circ g\circ k^n 
</math>
по [I.5]

'''Пример 1''' Аналогично предыдущему разделу, докажем
корректность итеративной факториальной функции.

<math>f=eq0\circ\bar{1}\rightarrow\bar{2};f\circ[subl\circ\bar{1}, \times]</math>

Мы хотим доказать, что <math>f:\langle x,1\rangle=x!</math>, причем тогда и
только тогда, когда <math>x</math> - целое неотрицательное число.

 Пусть
<math>p=eq\circ\bar{1}, g=\bar{2}, h=id, k=[subl\circ\bar{1}, \times]</math>.
тогда <math>f=p\circ g; h\circ f\circ k</math> и поэтому

<math>
\label{fi1} f=p\rightarrow g ;\ldots;p\circ k^n\rightarrow g\circ
k^n, \ldots
</math>

в силу теоремы об итерации, так как <math>h^n=id</math>.


Теперь покажем, что

<math>
\label{fi2}pair\rightarrow\rightarrow k^n=[a_n,b_n]
</math>

верно для любого значения <math>n\geq1</math>, где

<math>
\label{fi3}a_n=subl^n\circ\bar{1}
</math>

<math>
\label{fi4}b_n=/\times[subl^{n-1}\circ\bar{1},\ldots,subl\circ\bar{1},\bar{2}]
</math>

 Итак, \ref{fi2} имеет место для <math>n=1</math> по определению <math>k</math>.
 Предположим, что \ref{fi2} верно для некоторого <math>n\geq1</math>, и
 докажем, что это утверждение верно для n+1. Имеем

<math>
\label{fi5} pair\rightarrow\rightarrow k^{n+1}=k\circ
k^n=[subl\circ\bar{1}, \times]\circ[a_n,b_n]
</math>

поскольку \ref{fi2} справедливо для n. И поэтому
<math>
\label{fi6} pair\rightarrow\rightarrow k^{n+1}=[subl\circ
a_n\times\circ[a_n,b_n]] 
</math>
согласно [I.1] и [I.5]

 Для перехода от \ref{fi5} к \ref{fi6} нужно проверить, что когда
<math>a_n</math> или <math>b_n</math> порождает <math>\bot</math> в \ref{fi5} тоже самое имеет место
и в \ref{fi6}. Далее,
<math>
\label{fi7} subl\circ a_n=subl^{n+1}\circ\bar{1}=a_{n+1}
</math>
согласно [I.3]

<math>
\label{fi8}
\times\circ[a_n,b_n]&=/\times\circ[subl^n\circ\bar{1},\ldots,subl\circ\bar{1},\bar{1},\bar{2}]\\
                    &=b_{n+1} \textrm{ 
</math>


Сочетания \ref{fi6}, \ref{fi7}, \ref{fi8}  дает
<math>
 pair\rightarrow\rightarrow k^{n+1}=[a_{n+1}, b_{n+1}]  (9)
</math>

Итак, отношение \ref{fi2} справедливо для <math>n=1</math>, а также выполняется
при n+1. По индукции, оно справедливо для любого <math>n\geq1</math>. Теперь
\ref{fi2} дает для пар

<math>
 \bar{T}\circ k^n\rightarrow\rightarrow p\circ k^n&=eq0\circ\bar{1}\circ[a_n,b_n]\\
                                                =eq0\circ a_n\\
                                                =eq0\circ subl^n\circ\bar{1}
</math>

<math>
 \bar{T}\circ k^n\rightarrow\rightarrow g\circ k^n=\bar{2}\circ[a_n,b_n]\\
                                                =/\times\circ[subl^{n-1}\circ\bar{1},\ldots,subl\circ\bar{1},\bar{2}]
</math>

(в обоих случаях используется [I.5]). Далее, из \ref{fi1}
следует, что <math>f:\langle x,1\rangle</math> определено тогда и только тогда,
когда имеется такое значение n, что <math>p\circ k^i:\langle
x,1\rangle=F</math> для всех <math>i\leq n</math> и <math>p\circ k^n:\langle
x,1\rangle=T</math>, т.е., согласно \ref{fi10},  <math>eq0\circ subl^n:x=T</math>
т.е. <math>x=n</math> и <math>g\circ k^n:\langle x,1\rangle</math> определено; в таком
случае, согласно \ref{fi11},

<math>f:\langle x,1\rangle=/\times\langle 1,2,3,\ldots,x-1,x,1\rangle=n!</math>

а то именно то, что нам и требовалось доказать.